$\forall$$n$, $m$, $k$:$\mathbb{N}$, $f$:($\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<$$m$}}$), $g$:($\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<$$k$+1}}$). fadd($f$;$g$) $\in$ $\mathbb{N}$$_{\mbox{\scriptsize $<$$n$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<$$m$+$k$}}$